Definitions	sq_type(T), IdLnk, x:A. B(x), P  Q, guard(T), t  T, prop{i:l}, x. t(x), t.1, x(s), t.2
Lemmas	Id sq, Id wf, pi1 wf, pi2 wf